using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics;

namespace OpSatPlan.SatSolvers
{
	public class LingelingSolver : SatSolver
	{
		private bool?[] mModel;
		public LingelingSolver ()
		{
		}
		protected override bool IsSat(string[] lines)
        {
            bool sat;
            bool processNumbers;
            sat = false;
            processNumbers = false;
            List<bool?> model = new List<bool?>();

            foreach (string line in lines)
            {
                if (!processNumbers)
                {
                    if (line.Contains("c"))
                        continue;
                    if (line.Contains("s SATISFIABLE"))
                    {
                        processNumbers = true;
                        sat = true;
                    }
                }
                else
                {
                    string[] lits = line.Split(' ');
                    foreach (string lit in lits)
                    {
                        int value;
                        if (int.TryParse(lit, out value))
                        {
                            if (value == 0)
                            {
                                break;
                            }
                            else
                            {
                                model.Insert((int)Math.Abs(value) - 1, (value > 0) ? true : false);
                            }
                        }
                    }
                }
            }
			this.mModel = model.ToArray();
            return sat;
        }

        public override bool?[] Model
        {
            get { return this.mModel; }
        }

        public override string Name
        {
            get { return "lingeling"; }
        }
		protected override string ExecutableName
		{
			get { return "lingeling"; }
		}
        protected override string Arguments(string cnfFileName)
        {
            return cnfFileName;
        }

        public override void Reset()
        {
            this.mModel = null;
        }
	}
}

